E:Type, T, V:(IdIdType), M:(IdLnkIdType), pred?:(E(?E)),
info:(E((:Id  Id) + (:(:IdLnk  E)  Id))), init:(i:IdEState(T(i))),
Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )EState(T(i))EState(T(i))),
val:(e:Ekindcase(kind(e); a.V(loc(e),a); l,t.M(l,t) )), time:(E).
(e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 SWellFounded(pred!(e;e'))
 (e:E. state_after(e)  EState(T(loc(e)))) 

latex

Definitions	t  T, Id, x:A. B(x), loc(e), f(a), EState(T), x.A(x), x. t(x), t.2, x:A  B(x), P  Q, when-after(e;info;pred?;init;Trans;val;time), x:AB(x), s = t, state_after(e), Type, IdLnk, Unit, left + right, x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, kind(e), , pred(e), , first(e), b, A, pred!(e;e'), SWellFounded(R(x;y))
Lemmas	strongwellfounded wf, pred! wf, not wf, assert wf, first wf, pred wf, rationals wf, kind wf, Knd wf, kindcase wf, unit wf, IdLnk wf, when-after wf, pi2 wf, EState wf, loc wf, Id wf